T:Type, ll:(T List List), x:T. (x  concat(ll))  (l:T List. ((l  ll)  (x  l))) 

latex

Definitions

x. t(x), x:AB(x), [], Type, void, append(as; bs), concat(ll), cons(car; cdr), prop{i:l}, t  T, x.A(x), P  Q, P  Q, P  Q, False, x:A. B(x), P  Q, x:A  B(x), s = t, type List, x:A. B(x), P  Q, left + right, (x  l), A c B, guard(T), f(a), , {x:A| B(x)} , , A  B, A, a < b, ||as||, Y, rec-case(a) of [] => s | x::y => z.t(x;y;z), n + m, nth_tl(n;as), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), b, if a<b then c else d, n - m, tl(l), reduce(f; k; as), l[i], i z j, i <z j, hd(l), T, True

Lemmas

true wf, squash wf, l member wf, iff wf, concat wf, append wf, false wf, nil member, and functionality wrt iff, exists functionality wrt iff, iff functionality wrt iff, all functionality wrt iff, cons member, member append